COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	AXIOM BOARD: BOARD = CROSS(SIDE,SIDE)
C00004 ENDMK
C⊗;
AXIOM BOARD: BOARD = CROSS(SIDE,SIDE);;

AXIOM MBOARD: MBOARD = BOARD\{<0,0>,<7,7>};;

AXIOM SIDE: SIDE = INTERVAL(0,7);;

DECLARE INDCONST BOARD MBOARD SIDE ε SET;

DECLARE PREDCONST DOMINOE(SET);

AXIOM DOMINOE: ∀A. (DOMINOE(A) ≡ ∃B C.(A={B,C} ∧ ADJACENT(B,C)));;

AXIOM COVER:	∀D.(COVER(D) ≡ ∀A.(AεD ⊃ DOMINOE(A)) ∧ DISJOINT(D) ∧
			∀ B.(BεMBOARD ⊃ ∃A.(AεD ∧ BεA));;

AXIOM NEXT:	∀m n.(next(m,n) ≡ m = SUCC(n) ∨ n = SUCC(m));;

AXIOM ADJACENT:	∀a b.(ADJACENT(A,B) ≡ CAR(A)=CAR(B) ∧next(CDR(A),CDR(B)));;

DEFINE WHITE: ∀A.(WHITE(A) ≡ EVEN(CAR(A)+CDR(A))),
		White = {x|xεBoard ∧ WHITE(x)};;

DEFINE BLACK:	Black = Board \ White;;

DECLARE INDCONST ROWεSET;
DEFINE:		ROW = {A|∃n a.(A = <n,a> ∧ nεSIDE ∧ a={b|bεBOARD ∧ CDR(b) = n})};;

AXIOM LEMMA:
		card(SIDE) = 8,
		EVEN(8),
		∀x y.(xεBOARD ∧ yεBOARD ∧ ADJACENT(x,y) ⊃ WHITE(x) ≡ ¬WHITE(y)),
		∀A.(DOMINOE(A) ⊃ card(A∩White) = 1),
		∀A.(DOMINOE(A) ⊃ card(A∩Black) = 1),
		∀n.(nεSIDE ⊃ card(CROSS({n},SIDE)∩White)=4),
		∀n.(nεSIDE ⊃ card(apply(ROW,n))=8 ∧ card(apply(ROW,n)∩White)=4),